$\forall$$T_{1}$, $T_{2}$:Type, ${\it as}$:$T_{1}$ List, ${\it bs}$:$T_{2}$ List, $i$:$\mathbb{N}$.
\\[0ex]$i$$<\parallel$zip(${\it as}$;${\it bs}$)$\parallel$ $\Rightarrow$ zip(${\it as}$;${\it bs}$)[$i$] $=$ $\langle$${\it as}$[$i$]$,\,$${\it bs}$[$i$]$\rangle$ $\in$ $T_{1}$$\times$$T_{2}$